M:MsgA, k:Knd, x:Id. M:k may not read x   

latex

Definitions	false, t  T, Id, Knd, type List, x.A(x), P  Q, x:A. B(x), x. t(x), f(x), KindDeq, deq-member(eq;x;L), b, , Top, a:A fp B(a), x:AB(x), b, A, s = t, Prop, x:AB(x), P & Q, P  Q, Unit, left+right, MsgA, M:k may not read x, IdDeq, x  dom(f)
Lemmas	msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, not wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, deq-member wf, Kind-deq wf, fpf-ap wf, Knd wf, Id wf, id-deq wf, bfalse wf